KILLED



    


Runtime Complexity (full) proof of /tmp/tmpnWDfLr/OvConsOS_complete_GM.xml









The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(2^n, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 5190 ms)


↳2 BOUNDS(2^n, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)

a__U11(tt, V1) → a__U12(a__isNatList(V1))

a__U12(tt) → tt

a__U21(tt, V1) → a__U22(a__isNat(V1))

a__U22(tt) → tt

a__U31(tt, V) → a__U32(a__isNatList(V))

a__U32(tt) → tt

a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)

a__U42(tt, V2) → a__U43(a__isNatIList(V2))

a__U43(tt) → tt

a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)

a__U52(tt, V2) → a__U53(a__isNatList(V2))

a__U53(tt) → tt

a__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)

a__U62(tt, V2) → a__U63(a__isNatIList(V2))

a__U63(tt) → tt

a__U71(tt, L) → s(a__length(mark(L)))

a__U81(tt) → nil

a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))

a__and(tt, X) → mark(X)

a__isNat(0) → tt

a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)

a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)

a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)

a__isNatIList(zeros) → tt

a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatIListKind(nil) → tt

a__isNatIListKind(zeros) → tt

a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatKind(0) → tt

a__isNatKind(length(V1)) → a__isNatIListKind(V1)

a__isNatKind(s(V1)) → a__isNatKind(V1)

a__isNatList(nil) → tt

a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__length(nil) → 0

a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

a__take(0, IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))

a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)

mark(zeros) → a__zeros

mark(U11(X1, X2)) → a__U11(mark(X1), X2)

mark(U12(X)) → a__U12(mark(X))

mark(isNatList(X)) → a__isNatList(X)

mark(U21(X1, X2)) → a__U21(mark(X1), X2)

mark(U22(X)) → a__U22(mark(X))

mark(isNat(X)) → a__isNat(X)

mark(U31(X1, X2)) → a__U31(mark(X1), X2)

mark(U32(X)) → a__U32(mark(X))

mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)

mark(U42(X1, X2)) → a__U42(mark(X1), X2)

mark(U43(X)) → a__U43(mark(X))

mark(isNatIList(X)) → a__isNatIList(X)

mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)

mark(U52(X1, X2)) → a__U52(mark(X1), X2)

mark(U53(X)) → a__U53(mark(X))

mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)

mark(U62(X1, X2)) → a__U62(mark(X1), X2)

mark(U63(X)) → a__U63(mark(X))

mark(U71(X1, X2)) → a__U71(mark(X1), X2)

mark(length(X)) → a__length(mark(X))

mark(U81(X)) → a__U81(mark(X))

mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)

mark(take(X1, X2)) → a__take(mark(X1), mark(X2))

mark(and(X1, X2)) → a__and(mark(X1), X2)

mark(isNatIListKind(X)) → a__isNatIListKind(X)

mark(isNatKind(X)) → a__isNatKind(X)

mark(cons(X1, X2)) → cons(mark(X1), X2)

mark(0) → 0

mark(tt) → tt

mark(s(X)) → s(mark(X))

mark(nil) → nil

a__zeros → zeros

a__U11(X1, X2) → U11(X1, X2)

a__U12(X) → U12(X)

a__isNatList(X) → isNatList(X)

a__U21(X1, X2) → U21(X1, X2)

a__U22(X) → U22(X)

a__isNat(X) → isNat(X)

a__U31(X1, X2) → U31(X1, X2)

a__U32(X) → U32(X)

a__U41(X1, X2, X3) → U41(X1, X2, X3)

a__U42(X1, X2) → U42(X1, X2)

a__U43(X) → U43(X)

a__isNatIList(X) → isNatIList(X)

a__U51(X1, X2, X3) → U51(X1, X2, X3)

a__U52(X1, X2) → U52(X1, X2)

a__U53(X) → U53(X)

a__U61(X1, X2, X3) → U61(X1, X2, X3)

a__U62(X1, X2) → U62(X1, X2)

a__U63(X) → U63(X)

a__U71(X1, X2) → U71(X1, X2)

a__length(X) → length(X)

a__U81(X) → U81(X)

a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)

a__take(X1, X2) → take(X1, X2)

a__and(X1, X2) → and(X1, X2)

a__isNatIListKind(X) → isNatIListKind(X)

a__isNatKind(X) → isNatKind(X)

Rewrite Strategy: FULL




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
mark(length(cons(X11668440_5, X21668441_5))) →+ a__U71(a__and(a__and(a__isNatList(X21668441_5), isNatIListKind(X21668441_5)), and(isNat(mark(X11668440_5)), isNatKind(mark(X11668440_5)))), X21668441_5)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0].
The pumping substitution is [X11668440_5 / length(cons(X11668440_5, X21668441_5))].
The result substitution is [ ].

The rewrite sequence
mark(length(cons(X11668440_5, X21668441_5))) →+ a__U71(a__and(a__and(a__isNatList(X21668441_5), isNatIListKind(X21668441_5)), and(isNat(mark(X11668440_5)), isNatKind(mark(X11668440_5)))), X21668441_5)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,1,0].
The pumping substitution is [X11668440_5 / length(cons(X11668440_5, X21668441_5))].
The result substitution is [ ].





(2) BOUNDS(2^n, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__zeros → cons(0', zeros)

a__U11(tt, V1) → a__U12(a__isNatList(V1))

a__U12(tt) → tt

a__U21(tt, V1) → a__U22(a__isNat(V1))

a__U22(tt) → tt

a__U31(tt, V) → a__U32(a__isNatList(V))

a__U32(tt) → tt

a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)

a__U42(tt, V2) → a__U43(a__isNatIList(V2))

a__U43(tt) → tt

a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)

a__U52(tt, V2) → a__U53(a__isNatList(V2))

a__U53(tt) → tt

a__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)

a__U62(tt, V2) → a__U63(a__isNatIList(V2))

a__U63(tt) → tt

a__U71(tt, L) → s(a__length(mark(L)))

a__U81(tt) → nil

a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))

a__and(tt, X) → mark(X)

a__isNat(0') → tt

a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)

a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)

a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)

a__isNatIList(zeros) → tt

a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatIListKind(nil) → tt

a__isNatIListKind(zeros) → tt

a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatKind(0') → tt

a__isNatKind(length(V1)) → a__isNatIListKind(V1)

a__isNatKind(s(V1)) → a__isNatKind(V1)

a__isNatList(nil) → tt

a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__length(nil) → 0'

a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

a__take(0', IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))

a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)

mark(zeros) → a__zeros

mark(U11(X1, X2)) → a__U11(mark(X1), X2)

mark(U12(X)) → a__U12(mark(X))

mark(isNatList(X)) → a__isNatList(X)

mark(U21(X1, X2)) → a__U21(mark(X1), X2)

mark(U22(X)) → a__U22(mark(X))

mark(isNat(X)) → a__isNat(X)

mark(U31(X1, X2)) → a__U31(mark(X1), X2)

mark(U32(X)) → a__U32(mark(X))

mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)

mark(U42(X1, X2)) → a__U42(mark(X1), X2)

mark(U43(X)) → a__U43(mark(X))

mark(isNatIList(X)) → a__isNatIList(X)

mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)

mark(U52(X1, X2)) → a__U52(mark(X1), X2)

mark(U53(X)) → a__U53(mark(X))

mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)

mark(U62(X1, X2)) → a__U62(mark(X1), X2)

mark(U63(X)) → a__U63(mark(X))

mark(U71(X1, X2)) → a__U71(mark(X1), X2)

mark(length(X)) → a__length(mark(X))

mark(U81(X)) → a__U81(mark(X))

mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)

mark(take(X1, X2)) → a__take(mark(X1), mark(X2))

mark(and(X1, X2)) → a__and(mark(X1), X2)

mark(isNatIListKind(X)) → a__isNatIListKind(X)

mark(isNatKind(X)) → a__isNatKind(X)

mark(cons(X1, X2)) → cons(mark(X1), X2)

mark(0') → 0'

mark(tt) → tt

mark(s(X)) → s(mark(X))

mark(nil) → nil

a__zeros → zeros

a__U11(X1, X2) → U11(X1, X2)

a__U12(X) → U12(X)

a__isNatList(X) → isNatList(X)

a__U21(X1, X2) → U21(X1, X2)

a__U22(X) → U22(X)

a__isNat(X) → isNat(X)

a__U31(X1, X2) → U31(X1, X2)

a__U32(X) → U32(X)

a__U41(X1, X2, X3) → U41(X1, X2, X3)

a__U42(X1, X2) → U42(X1, X2)

a__U43(X) → U43(X)

a__isNatIList(X) → isNatIList(X)

a__U51(X1, X2, X3) → U51(X1, X2, X3)

a__U52(X1, X2) → U52(X1, X2)

a__U53(X) → U53(X)

a__U61(X1, X2, X3) → U61(X1, X2, X3)

a__U62(X1, X2) → U62(X1, X2)

a__U63(X) → U63(X)

a__U71(X1, X2) → U71(X1, X2)

a__length(X) → length(X)

a__U81(X) → U81(X)

a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)

a__take(X1, X2) → take(X1, X2)

a__and(X1, X2) → and(X1, X2)

a__isNatIListKind(X) → isNatIListKind(X)

a__isNatKind(X) → isNatKind(X)

S is empty.
Rewrite Strategy: FULL




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
TRS:
Rules:
a__zeros → cons(0', zeros)
a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))
a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)
a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tt
a__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)
a__U62(tt, V2) → a__U63(a__isNatIList(V2))
a__U63(tt) → tt
a__U71(tt, L) → s(a__length(mark(L)))
a__U81(tt) → nil
a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__and(tt, X) → mark(X)
a__isNat(0') → tt
a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tt
a__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0') → tt
a__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0'
a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
a__take(0', IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))
a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(U63(X)) → a__U63(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U81(X)) → a__U81(mark(X))
mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0') → 0'
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)
a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isNat(X) → isNat(X)
a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)
a__U53(X) → U53(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__U63(X) → U63(X)
a__U71(X1, X2) → U71(X1, X2)
a__length(X) → length(X)
a__U81(X) → U81(X)
a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Types:
a__zeros :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
cons :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
0' :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
zeros :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U11 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
tt :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U12 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U21 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U22 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNat :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U31 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U32 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U41 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U42 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U43 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatIList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U51 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U52 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U53 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U61 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U62 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U63 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U71 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
s :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__length :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
mark :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U81 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
nil :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U91 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
take :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__and :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
length :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatIListKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatIListKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
and :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNat :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__take :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U11 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U12 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U21 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U22 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U31 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U32 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U41 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U42 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U43 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatIList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U51 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U52 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U53 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U61 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U62 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U63 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U71 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U81 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U91 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
hole_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U911_0 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
gen_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U912_0 :: Nat → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__U11, a__isNatList, a__U21, a__isNat, a__U31, a__U41, a__U42, a__isNatIList, a__U51, a__U52, a__U61, a__U62, a__U71, a__length, mark, a__U91, a__and, a__isNatIListKind, a__isNatKind
They will be analysed ascendingly in the following order:
a__U11 = a__isNatList
a__U11 = a__U21
a__U11 = a__isNat
a__U11 = a__U31
a__U11 = a__U41
a__U11 = a__U42
a__U11 = a__isNatIList
a__U11 = a__U51
a__U11 = a__U52
a__U11 = a__U61
a__U11 = a__U62
a__U11 = a__U71
a__U11 = a__length
a__U11 = mark
a__U11 = a__U91
a__U11 = a__and
a__U11 = a__isNatIListKind
a__U11 = a__isNatKind
a__isNatList = a__U21
a__isNatList = a__isNat
a__isNatList = a__U31
a__isNatList = a__U41
a__isNatList = a__U42
a__isNatList = a__isNatIList
a__isNatList = a__U51
a__isNatList = a__U52
a__isNatList = a__U61
a__isNatList = a__U62
a__isNatList = a__U71
a__isNatList = a__length
a__isNatList = mark
a__isNatList = a__U91
a__isNatList = a__and
a__isNatList = a__isNatIListKind
a__isNatList = a__isNatKind
a__U21 = a__isNat
a__U21 = a__U31
a__U21 = a__U41
a__U21 = a__U42
a__U21 = a__isNatIList
a__U21 = a__U51
a__U21 = a__U52
a__U21 = a__U61
a__U21 = a__U62
a__U21 = a__U71
a__U21 = a__length
a__U21 = mark
a__U21 = a__U91
a__U21 = a__and
a__U21 = a__isNatIListKind
a__U21 = a__isNatKind
a__isNat = a__U31
a__isNat = a__U41
a__isNat = a__U42
a__isNat = a__isNatIList
a__isNat = a__U51
a__isNat = a__U52
a__isNat = a__U61
a__isNat = a__U62
a__isNat = a__U71
a__isNat = a__length
a__isNat = mark
a__isNat = a__U91
a__isNat = a__and
a__isNat = a__isNatIListKind
a__isNat = a__isNatKind
a__U31 = a__U41
a__U31 = a__U42
a__U31 = a__isNatIList
a__U31 = a__U51
a__U31 = a__U52
a__U31 = a__U61
a__U31 = a__U62
a__U31 = a__U71
a__U31 = a__length
a__U31 = mark
a__U31 = a__U91
a__U31 = a__and
a__U31 = a__isNatIListKind
a__U31 = a__isNatKind
a__U41 = a__U42
a__U41 = a__isNatIList
a__U41 = a__U51
a__U41 = a__U52
a__U41 = a__U61
a__U41 = a__U62
a__U41 = a__U71
a__U41 = a__length
a__U41 = mark
a__U41 = a__U91
a__U41 = a__and
a__U41 = a__isNatIListKind
a__U41 = a__isNatKind
a__U42 = a__isNatIList
a__U42 = a__U51
a__U42 = a__U52
a__U42 = a__U61
a__U42 = a__U62
a__U42 = a__U71
a__U42 = a__length
a__U42 = mark
a__U42 = a__U91
a__U42 = a__and
a__U42 = a__isNatIListKind
a__U42 = a__isNatKind
a__isNatIList = a__U51
a__isNatIList = a__U52
a__isNatIList = a__U61
a__isNatIList = a__U62
a__isNatIList = a__U71
a__isNatIList = a__length
a__isNatIList = mark
a__isNatIList = a__U91
a__isNatIList = a__and
a__isNatIList = a__isNatIListKind
a__isNatIList = a__isNatKind
a__U51 = a__U52
a__U51 = a__U61
a__U51 = a__U62
a__U51 = a__U71
a__U51 = a__length
a__U51 = mark
a__U51 = a__U91
a__U51 = a__and
a__U51 = a__isNatIListKind
a__U51 = a__isNatKind
a__U52 = a__U61
a__U52 = a__U62
a__U52 = a__U71
a__U52 = a__length
a__U52 = mark
a__U52 = a__U91
a__U52 = a__and
a__U52 = a__isNatIListKind
a__U52 = a__isNatKind
a__U61 = a__U62
a__U61 = a__U71
a__U61 = a__length
a__U61 = mark
a__U61 = a__U91
a__U61 = a__and
a__U61 = a__isNatIListKind
a__U61 = a__isNatKind
a__U62 = a__U71
a__U62 = a__length
a__U62 = mark
a__U62 = a__U91
a__U62 = a__and
a__U62 = a__isNatIListKind
a__U62 = a__isNatKind
a__U71 = a__length
a__U71 = mark
a__U71 = a__U91
a__U71 = a__and
a__U71 = a__isNatIListKind
a__U71 = a__isNatKind
a__length = mark
a__length = a__U91
a__length = a__and
a__length = a__isNatIListKind
a__length = a__isNatKind
mark = a__U91
mark = a__and
mark = a__isNatIListKind
mark = a__isNatKind
a__U91 = a__and
a__U91 = a__isNatIListKind
a__U91 = a__isNatKind
a__and = a__isNatIListKind
a__and = a__isNatKind
a__isNatIListKind = a__isNatKind




(8) Obligation:
TRS:
Rules:
a__zeros → cons(0', zeros)
a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))
a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)
a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tt
a__U61(tt, V1, V2) → a__U62(a__isNat(V1), V2)
a__U62(tt, V2) → a__U63(a__isNatIList(V2))
a__U63(tt) → tt
a__U71(tt, L) → s(a__length(mark(L)))
a__U81(tt) → nil
a__U91(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__and(tt, X) → mark(X)
a__isNat(0') → tt
a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tt
a__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatIListKind(take(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0') → tt
a__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatList(take(V1, V2)) → a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0'
a__length(cons(N, L)) → a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
a__take(0', IL) → a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL)))
a__take(s(M), cons(N, IL)) → a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(U63(X)) → a__U63(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U81(X)) → a__U81(mark(X))
mark(U91(X1, X2, X3, X4)) → a__U91(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0') → 0'
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)
a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isNat(X) → isNat(X)
a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)
a__U53(X) → U53(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__U63(X) → U63(X)
a__U71(X1, X2) → U71(X1, X2)
a__length(X) → length(X)
a__U81(X) → U81(X)
a__U91(X1, X2, X3, X4) → U91(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Types:
a__zeros :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
cons :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
0' :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
zeros :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U11 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
tt :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U12 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U21 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U22 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNat :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U31 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U32 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U41 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U42 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U43 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatIList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U51 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U52 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U53 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U61 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U62 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U63 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U71 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
s :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__length :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
mark :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U81 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
nil :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__U91 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
take :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__and :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
length :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatIListKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__isNatKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatIListKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
and :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNat :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatKind :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
a__take :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U11 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U12 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U21 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U22 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U31 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U32 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U41 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U42 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U43 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
isNatIList :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U51 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U52 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U53 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U61 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U62 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U63 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U71 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U81 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
U91 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91 → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
hole_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U911_0 :: 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
gen_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U912_0 :: Nat → 0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U91
Generator Equations:
gen_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U912_0(0) ⇔ 0'
gen_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U912_0(+(x, 1)) ⇔ cons(gen_0':zeros:cons:tt:s:nil:take:length:isNatIListKind:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61:U62:U63:U71:U81:U912_0(x), 0')
The following defined symbols remain to be analysed:
a__isNatList, a__U11, a__U21, a__isNat, a__U31, a__U41, a__U42, a__isNatIList, a__U51, a__U52, a__U61, a__U62, a__U71, a__length, mark, a__U91, a__and, a__isNatIListKind, a__isNatKind
They will be analysed ascendingly in the following order:
a__U11 = a__isNatList
a__U11 = a__U21
a__U11 = a__isNat
a__U11 = a__U31
a__U11 = a__U41
a__U11 = a__U42
a__U11 = a__isNatIList
a__U11 = a__U51
a__U11 = a__U52
a__U11 = a__U61
a__U11 = a__U62
a__U11 = a__U71
a__U11 = a__length
a__U11 = mark
a__U11 = a__U91
a__U11 = a__and
a__U11 = a__isNatIListKind
a__U11 = a__isNatKind
a__isNatList = a__U21
a__isNatList = a__isNat
a__isNatList = a__U31
a__isNatList = a__U41
a__isNatList = a__U42
a__isNatList = a__isNatIList
a__isNatList = a__U51
a__isNatList = a__U52
a__isNatList = a__U61
a__isNatList = a__U62
a__isNatList = a__U71
a__isNatList = a__length
a__isNatList = mark
a__isNatList = a__U91
a__isNatList = a__and
a__isNatList = a__isNatIListKind
a__isNatList = a__isNatKind
a__U21 = a__isNat
a__U21 = a__U31
a__U21 = a__U41
a__U21 = a__U42
a__U21 = a__isNatIList
a__U21 = a__U51
a__U21 = a__U52
a__U21 = a__U61
a__U21 = a__U62
a__U21 = a__U71
a__U21 = a__length
a__U21 = mark
a__U21 = a__U91
a__U21 = a__and
a__U21 = a__isNatIListKind
a__U21 = a__isNatKind
a__isNat = a__U31
a__isNat = a__U41
a__isNat = a__U42
a__isNat = a__isNatIList
a__isNat = a__U51
a__isNat = a__U52
a__isNat = a__U61
a__isNat = a__U62
a__isNat = a__U71
a__isNat = a__length
a__isNat = mark
a__isNat = a__U91
a__isNat = a__and
a__isNat = a__isNatIListKind
a__isNat = a__isNatKind
a__U31 = a__U41
a__U31 = a__U42
a__U31 = a__isNatIList
a__U31 = a__U51
a__U31 = a__U52
a__U31 = a__U61
a__U31 = a__U62
a__U31 = a__U71
a__U31 = a__length
a__U31 = mark
a__U31 = a__U91
a__U31 = a__and
a__U31 = a__isNatIListKind
a__U31 = a__isNatKind
a__U41 = a__U42
a__U41 = a__isNatIList
a__U41 = a__U51
a__U41 = a__U52
a__U41 = a__U61
a__U41 = a__U62
a__U41 = a__U71
a__U41 = a__length
a__U41 = mark
a__U41 = a__U91
a__U41 = a__and
a__U41 = a__isNatIListKind
a__U41 = a__isNatKind
a__U42 = a__isNatIList
a__U42 = a__U51
a__U42 = a__U52
a__U42 = a__U61
a__U42 = a__U62
a__U42 = a__U71
a__U42 = a__length
a__U42 = mark
a__U42 = a__U91
a__U42 = a__and
a__U42 = a__isNatIListKind
a__U42 = a__isNatKind
a__isNatIList = a__U51
a__isNatIList = a__U52
a__isNatIList = a__U61
a__isNatIList = a__U62
a__isNatIList = a__U71
a__isNatIList = a__length
a__isNatIList = mark
a__isNatIList = a__U91
a__isNatIList = a__and
a__isNatIList = a__isNatIListKind
a__isNatIList = a__isNatKind
a__U51 = a__U52
a__U51 = a__U61
a__U51 = a__U62
a__U51 = a__U71
a__U51 = a__length
a__U51 = mark
a__U51 = a__U91
a__U51 = a__and
a__U51 = a__isNatIListKind
a__U51 = a__isNatKind
a__U52 = a__U61
a__U52 = a__U62
a__U52 = a__U71
a__U52 = a__length
a__U52 = mark
a__U52 = a__U91
a__U52 = a__and
a__U52 = a__isNatIListKind
a__U52 = a__isNatKind
a__U61 = a__U62
a__U61 = a__U71
a__U61 = a__length
a__U61 = mark
a__U61 = a__U91
a__U61 = a__and
a__U61 = a__isNatIListKind
a__U61 = a__isNatKind
a__U62 = a__U71
a__U62 = a__length
a__U62 = mark
a__U62 = a__U91
a__U62 = a__and
a__U62 = a__isNatIListKind
a__U62 = a__isNatKind
a__U71 = a__length
a__U71 = mark
a__U71 = a__U91
a__U71 = a__and
a__U71 = a__isNatIListKind
a__U71 = a__isNatKind
a__length = mark
a__length = a__U91
a__length = a__and
a__length = a__isNatIListKind
a__length = a__isNatKind
mark = a__U91
mark = a__and
mark = a__isNatIListKind
mark = a__isNatKind
a__U91 = a__and
a__U91 = a__isNatIListKind
a__U91 = a__isNatKind
a__and = a__isNatIListKind
a__and = a__isNatKind
a__isNatIListKind = a__isNatKind